Search Results

Documents authored by Scagnetto, Ivan

Document
DOI: 10.4230/LIPIcs.TYPES.2020.7
Λ-Symsym: An Interactive Tool for Playing with Involutions and Types

Authors: Furio Honsell, Marina Lenisa, and Ivan Scagnetto

Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)

Abstract
We present the web portal Λ-symsym, available at http://158.110.146.197:31780/automata/, for experimenting with game semantics of λ^!-calculus, and its normalizing elementary sub-calculus, the λ^{EAL}-calculus. The λ^!-calculus is a generalization of the λ-calculus obtained by introducing a modal operator !, giving rise to a pattern β-reduction. Its sub-calculus corresponds to an applicatively closed class of terms normalizing in an elementary number of steps, in which all elementary functions can be encoded. The game model which we consider is the Geometry of Interaction model I introduced by Abramsky to study reversible computations, consisting of partial involutions over a very simple language of moves. Given a λ^!- or a λ^{EAL}-term, M, Λ-symsym provides: - an abstraction algorithm A^!, for compiling M into a term, A^!(M), of the linear combinatory logic CL^{!}, or the normalizing combinatory logic CL^{EAL}; - an interpretation algorithm [[ ]]^I yielding a specification of the partial involution [[A^!(M)]]^I in the model I; - an algorithm, I2T, for synthesizing from [[A^!(M)]]^I a type, I2T([[A^!(M)]]^I), in a multimodal, intersection type assignment discipline, ⊢_!. - an algorithm, T2I, for synthesizing a specification of a partial involution from a type in ⊢_!, which is an inverse to the former. We conjecture that ⊢_! M : I2T([[A^!(M)]]^I). Λ-symsym permits to investigate experimentally the fine structure of I, and hence the game semantics of the λ^!- and λ^{EAL}-calculi. For instance, we can easily verify that the model I is a λ^!-algebra in the case of strictly linear λ-terms, by checking all the necessary equations, and find counterexamples in the general case. We make this tool available for readers interested to play with games (-semantics). The paper builds on earlier work by the authors, the type system being an improvement.
Cite as

Furio Honsell, Marina Lenisa, and Ivan Scagnetto. Λ-Symsym: An Interactive Tool for Playing with Involutions and Types. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{honsell_et_al:LIPIcs.TYPES.2020.7,
  author =	{Honsell, Furio and Lenisa, Marina and Scagnetto, Ivan},
  title =	{{\Lambda-Symsym: An Interactive Tool for Playing with Involutions and Types}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.7},
  URN =		{urn:nbn:de:0030-drops-138867},
  doi =		{10.4230/LIPIcs.TYPES.2020.7},
  annote =	{Keywords: game semantics, lambda calculus, involutions, linear logic, implicit computational complexity}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.15
lambda!-calculus, Intersection Types, and Involutions

Authors: Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, and Ivan Scagnetto

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
Abramsky’s affine combinatory algebras are models of affine combinatory logic, which refines standard combinatory logic in the direction of Linear Logic. Abramsky introduced various universal models of computation based on affine combinatory algebras, consisting of partial involutions over a suitable formal language {of moves}, in order to discuss reversible computation in a Geometry of Interaction setting. We investigate partial involutions from the point of view of the model theory of lambda!-calculus. The latter is a refinement of the standard lambda-calculus, corresponding to affine combinatory logic. We introduce intersection type systems for the lambda!-calculus, by extending standard intersection types with a !_u-operator. These induce affine combinatory algebras, and, via suitable quotients, models of the lambda!-calculus. In particular, we introduce an intersection type system for assigning principal types to lambda!-terms, and we state a correspondence between the partial involution interpreting a combinator and the principal type of the corresponding lambda!-term. This analogy allows for explaining as unification between principal types the somewhat awkward linear application of involutions arising from Geometry of Interaction.
Cite as

Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, and Ivan Scagnetto. lambda!-calculus, Intersection Types, and Involutions. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{ciaffaglione_et_al:LIPIcs.FSCD.2019.15,
  author =	{Ciaffaglione, Alberto and Di Gianantonio, Pietro and Honsell, Furio and Lenisa, Marina and Scagnetto, Ivan},
  title =	{{lambda!-calculus, Intersection Types, and Involutions}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{15:1--15:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.15},
  URN =		{urn:nbn:de:0030-drops-105228},
  doi =		{10.4230/LIPIcs.FSCD.2019.15},
  annote =	{Keywords: Affine Combinatory Algebra, Affine Lambda-calculus, Intersection Types, Geometry of Interaction}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2018.37
The Delta-Framework

Authors: Furio Honsell, Luigi Liquori, Claude Stolze, and Ivan Scagnetto

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
We introduce the Delta-framework, LF_Delta, a dependent type theory based on the Edinburgh Logical Framework LF, extended with the strong proof-functional connectives, i.e. strong intersection, minimal relevant implication and strong union. Strong proof-functional connectives take into account the shape of logical proofs, thus reflecting polymorphic features of proofs in formulae. This is in contrast to classical or intuitionistic connectives where the meaning of a compound formula depends only on the truth value or the provability of its subformulae. Our framework encompasses a wide range of type disciplines. Moreover, since relevant implication permits to express subtyping, LF_Delta subsumes also Pfenning's refinement types. We discuss the design decisions which have led us to the formulation of LF_Delta, study its metatheory, and provide various examples of applications. Our strong proof-functional type theory can be plugged in existing common proof assistants.
Cite as

Furio Honsell, Luigi Liquori, Claude Stolze, and Ivan Scagnetto. The Delta-Framework. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 37:1-37:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{honsell_et_al:LIPIcs.FSTTCS.2018.37,
  author =	{Honsell, Furio and Liquori, Luigi and Stolze, Claude and Scagnetto, Ivan},
  title =	{{The Delta-Framework}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{37:1--37:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.37},
  URN =		{urn:nbn:de:0030-drops-99367},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.37},
  annote =	{Keywords: Logic of programs, type theory, lambda-calculus}
}
Document
DOI: 10.4230/DagSemProc.09101.3
Context Aware Browser

Authors: Stefano Mizzaro, Paolo Coppola, Vincenzo Della Mea, Luca Di Gaspero, Danny Mischis, Elena Nazzi, Ivan Scagnetto, and Luca Vassena

Published in: Dagstuhl Seminar Proceedings, Volume 9101, Interactive Information Retrieval (2009)

Abstract
I will present the Context Aware Browser, a novel paradigm for context-aware access to Web contents with mobile devices. The idea is to allow automatic download of Web pages, and even automatic execution of Web applications, on user's own mobile device. The Web resources are not simply pushed on the mobile device; rather, they are selected on the basis of the context the user is in: context data (mainly location, but not only) are used to build a query sent to an external search engine, that selects the most relevant Web content. I will describe the idea, provide some examples, show a video of a recently built prototype, present implementation issues, discuss our specific evaluation methodology and the results, and sketch future work and problems. This is an ongoing project, started about five years ago; it is joint work with the Context Aware and Mobile Systems laboratory (smdc.uniud.it) and the MoBe spinoff (www.mobe.it) at Udine University.
Cite as

Stefano Mizzaro, Paolo Coppola, Vincenzo Della Mea, Luca Di Gaspero, Danny Mischis, Elena Nazzi, Ivan Scagnetto, and Luca Vassena. Context Aware Browser. In Interactive Information Retrieval. Dagstuhl Seminar Proceedings, Volume 9101, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{mizzaro_et_al:DagSemProc.09101.3,
  author =	{Mizzaro, Stefano and Coppola, Paolo and Della Mea, Vincenzo and Di Gaspero, Luca and Mischis, Danny and Nazzi, Elena and Scagnetto, Ivan and Vassena, Luca},
  title =	{{Context Aware Browser}},
  booktitle =	{Interactive Information Retrieval},
  pages =	{1--23},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9101},
  editor =	{Nicholas J. Belkin and Norbert Fuhr and Joemon Jose and C. J. Keith van Rijsbergen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09101.3},
  URN =		{urn:nbn:de:0030-drops-21515},
  doi =		{10.4230/DagSemProc.09101.3},
  annote =	{Keywords: Context-aware, information retrieval, mobile devices}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact